$\forall$$T$, $X$:Type, ${\it eq}$:EqDecider($X$), $f$, $g$:$x$:$X$ fp$\rightarrow$ Type, $x$:$X$. $g$ $\subseteq$ $f$ $\Rightarrow$ $f$($x$)?$T$ $\subseteq\rho$ $g$($x$)?Top